perm filename RAT.LAN[EKL,SYS] blob
sn#860112 filedate 1988-08-17 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00010 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 the field of rationals there are some bugs to clean
C00005 00003 ordering of rationals
C00013 00004 addition of rationals
C00017 00005 multiplication of rationals
C00022 00006 the canonical map Z-→r
C00026 00007 *--→ noleastrat follows from noleastfr as follows:
C00037 00008 main property of addition
C00040 00009 commaddrat
C00053 00010 main property of multiplication
C00066 ENDMK
C⊗;
;the field of rationals ;there are some bugs to clean
(wipe-out)
(get-proofs frac prf ekl sys)
;equivalence classes of fractions
(proof rational)
(decl (r r0 r1 r2) (type: |@Q→TRUTHVAL|) (sort: RATIO))
;labels: SET_EXTENSIONALITY
;∀SETVAR SETVAR1.(∀ARB.ARBεSETVAR≡ARBεSETVAR1)⊃SETVAR=SETVAR1
;(ue ((setvar.r)(setvar1.r1)) set_extensionality)
;(∀ARB.ARBεr≡ARBεr1)⊃r=r1
;(label ratext)
;(axiom |∀arb r.r(arb)⊃fr(arb)|)
;(label ratsort)(label simpinfo)
(axiom |∀r r1.(∀q.r(q)≡r1(q))⊃r=r1|)
(label ratio_extensionality)
;equivalence classes and representatives
(decl (eqclass) (type: |@Q→@R|))
(define eqclass |∀q.eqclass(q)=λq0.ef(q0,q)|)
(axiom |∀q.ratio(eqclass(q))|)
(label mkratio)(label simpinfo)
(axiom |∀r.∃q.r=eqclass(q)|)
(label ratiodef)
(decl represent (type: |@r→@q|))
(define represent |∀r.eqclass(represent(r))=r| (ratiodef choice))
(label representdef)
(axiom |∀r.fr represent(r)|)
(label simpinfo)
;(trw |(eqclass represent(r))(represent r)| (open eqclass) reflexf)
;(rw * representdef)
;REPRESENT(r)εr
(axiom |∀r.r(represent(r))|)
(label simpinfo)
(axiom |∀q.ef(represent(eqclass q),q)|)
(label mkrepresent)
;see proof below
(axiom |∀r r1.ef(represent r,represent r1)≡r=r1|)
(label represent_uniqueness)
;see proof below
(axiom |∀q q0.ef(q,q0)≡eqclass q=eqclass q0|)
(label eqclass_uniqueness)
;see proof below
(show *)
;ordering of rationals
(proof ordrat)
;Landau_def18
(decl greatrat (type: |@r⊗@r→truthval|) (infixname: |>>|)
(syntype: constant) (bindingpower: 945))
(define greatrat |∀r r1.r>>r1=gf(represent(r),represent(r1))|)
;Landau_def19
(decl lessrat (type: |@r⊗@r→truthval|) (infixname: |<<|)
(syntype: constant) (bindingpower: 945))
(define lessrat |∀r r1.r<<r1=lf(represent(r),represent(r1))|)
;Landau_th81
;(trw |∀r r1.r << r1 ∨ r = r1 ∨ r >> r1|
; totalordfr (open greatrat lessrat)
; (use represent_uniqueness mode: exact direction: reverse))
;∀r r1.r << r1∨r=r1∨r >> r1
(axiom |∀r r1.r<<r1∨r=r1∨r>>r1|)
(label totalordrat)
;(trw |∀r r1.r = r1 ⊃ ¬r << r1 ∧ ¬r >> r1|
; strictfr1 (open greatrat lessrat)
; (use represent_uniqueness mode: exact direction: reverse))
;∀r r1.r=r1⊃¬r << r1∧¬r >> r1
(axiom |∀r r1.r = r1 ⊃ ¬r << r1 ∧ ¬r >> r1|)
(label strictrat1)
;(trw |∀r r1.r >> r1 ⊃ ¬r = r1 ∧ ¬r << r1|
; strictfr2 (open greatrat lessrat)
; (use represent_uniqueness mode: exact direction: reverse))
;∀r r1.r >> r1⊃¬r=r1∧¬r << r1
(axiom |∀r r1.r >> r1 ⊃ ¬r = r1 ∧ ¬r << r1|)
(label strictrat2)
;(trw |∀r r1.r << r1 ⊃ ¬r = r1 ∧ ¬r >> r1|
; strictfr3 (open greatrat lessrat)
; (use represent_uniqueness mode: exact direction: reverse))
;∀r r1.r << r1⊃¬r=r1∧¬r >> r1
(axiom |∀r r1.r << r1 ⊃ ¬r = r1 ∧ ¬r >> r1|)
(label strictrat3)
(axiom |∀r r0.r<<r0⊃¬r=r0|)
(label strictlylessrat)
;see proof below
;Landau_th 82 83
;(trw |∀r r1.r>>r1≡r1<<r| (open lessrat greatrat) gf_lf)
;∀r r1.r >> r1≡r1 << r
(axiom |∀r r1.r>>r1≡r1<<r|)
(label grat_lrat)
;(trw |r<<r0⊃¬r0<<r| (open lessrat) antisymless)
(axiom |∀r r0.r<<r0⊃¬r0<<r|)
(label simpinfo)(label antisymlessrat)
;Landau_def20
(decl geqrat (type: |@r⊗@r→truthval|) (infixname: |>=|)
(syntype: constant) (bindingpower: 945))
(define geqrat |∀r r1.r >= r1 ≡ (r=r1 ∨ r >> r1)|)
;Landau_def21
(decl leqrat (type: |@r⊗@r→truthval|) (infixname: |=<|)
(syntype: constant) (bindingpower: 945))
(define leqrat |∀r r1.r =< r1 ≡ (r=r1 ∨ r << r1)|)
;(trw |∀r r1.leqrat(r,r1)≡lef(represent r,represent r1)| (open leqrat)
; (use represent_uniqueness mode: exact direction: reverse))
;∀r r1.r =< r1≡LEF(REPRESENT(r),REPRESENT(r1))
(axiom |∀r r1.r =< r1≡lef(represent(r),represent(r1))|)
(label leqratdef1)
;(trw |∀r r1.geqrat(r,r1)≡gef(represent r,represent r1)| (open geqrat)
; (use represent_uniqueness mode: exact direction: reverse))
;∀r r1.r >= r1≡GEF(REPRESENT(r),REPRESENT(r1))
(axiom |∀r r1.r >= r1≡gef(represent(r),represent(r1))|)
(label geqratdef1)
;Landau_th84 85
;(trw |∀r r1.r >= r1 ≡ r1 =< r| gef_lef
; (use leqratdef1 geqratdef1 mode: exact))
;∀r r1.r >= r1≡r1 =< r
(axiom |∀r r1.r >= r1≡r1 =< r|)
(label geqrat_leqrat)
;Landau_th86
;(trw |∀r r1 r2.r<<r1∧r1<<r2⊃r<<r2| (open lessrat)(use transordfr))
;∀r r1 r2.r << r1∧r1 << r2⊃r << r2
(axiom |∀r r1 r2.r<<r1∧r1<<r2⊃r<<r2|)
(label transordrat)
;Landau_th87
;(trw |∀r r1 r2.r=<r1 ∧ r1 << r2 ⊃ r << r2| (open lessrat)
; (use leqratdef1 mode: exact)
; (use landau_a_th51 ue: ((r. |represent r|)
; (r1.|represent r1|)
; (r2.|represent r2|)) mode: exact))
;∀r r1 r2.r =< r1∧r1 << r2⊃r << r2
(axiom |∀r r1 r2.r =< r1∧r1 << r2⊃r << r2|)
(label landau_a_th87)
(axiom |∀r r1 r2.r << r1∧r1 =< r2⊃r << r2|)
(label landau_b_th87)
;as above
;Landau_th88
;(trw |∀r r1 r2.r =< r1∧r1 =< r2⊃r =< r2| landau_th52
; (use leqratdef1 mode: exact))
;∀r r1 r2.r =< r1∧r1 =< r2⊃r =< r2
(axiom |∀r r1 r2.r =< r1∧r1 =< r2⊃r =< r2|)
(label landau_th88)
;Landau_th89
;(trw |∀r ∃r1.r<<r1| (open lessrat) nolastfr)
(axiom |∀r.∃r1.r1>>r|)
(label nolastrat)
;exercise
;Landau_th90
(axiom |∀r. ∃r0.r0<<r|)
(label noleastrat)
;see proof below
;Landau_th91
(axiom |∀r r1.∃r0.r<<r1⊃r<<r0∧r0<<r1|)
(label denserat)
;see proof below
;zero
(define qzero |qzero=eqclass rz|)
(decl rzerop (type: |@r→truthval|) (syntype: constant))
(define rzerop |rzerop=(λr.represent r=qz)|)
(label rzeropdef)
;(define rzerop |∀r.rzerop(r)=ef(represent r,qz)|)
;(label rzeropdef)
;one
(define rone |rone=eqclass qone|)
(decl ronep (type: |@r→truthval|) (syntype: constant))
(define ronep |ronep=(λr.represent r=qone)|)
(label ronedef)
;(define ronep |∀r.ronep(r)=ef(represent r,qone)|)
;(trw |∀r r0.rzerop r0⊃¬r<<r0| (open lessrat rzerop lf)
; (use timesfacts mode: exact) zeroleast1)
;∀r r0.rZEROP1(r0)⊃¬r << r0
(axiom |∀r r0.rzerop r0⊃¬r<<r0|)
(label rzeroleast)
(axiom |∀r.rzero =< r|)
(label rzeroleast2)(label simpinfo)
(show *)
;addition of rationals
(proof addrat)
;Landau_def22
(decl addrat (type: |@r*→@r|) (infixname: |++|) (bindingpower: 948))
(defax addrat |∀r r0.(r++r0)=(eqclass(pf(represent r,represent r0)))|)
(label addrat)
;(trw |∀r r0.ratio(r++r0)| (open addrat))
;∀r r0.RATIO(r ++ r0)
(axiom |∀r r0.ratio(r++r0)|)
(label simpinfo)
;(trw |ef(represent(r++r1),pf(represent r,represent r1))| (open addrat)
; (use mkrepresent ))
;EF(REPRESENT(r ++ r1),PF(REPRESENT(r),REPRESENT(r1)))
(axiom |∀r r1.ef(represent(r++r1),pf(represent r,represent r1))|)
(label represent_ratsum)
(axiom |∀q q1.(eqclass q ++ eqclass q1)=eqclass(pf(q,q1))|)
(label addrat_reduction)
;see proof below
;Landau_th92
(axiom |∀r r0.r++r0=r0++r|)
(label commaddrat)
;see proof below
;Landau_th93
(axiom |∀r r0 r1.(r++r0)++r1=r++(r0++r1)|)
(label assocaddrat)
;see proof below
;Landau_th94
(axiom |∀r r1.¬rzerop(r1)⊃(r++r1)>>r|)
(label addrat_increasing)
;see proof below
;Landau_th95
(axiom |∀r r0 r1.r>>r0⊃(r++r1)>>(r0++r1)|)
(label great_addratpreserving)
;see proof below
;Landau_th96
(axiom |∀r r0 r1.r=r0⊃(r++r1)=(r0++r1)|)
(label great_addratpreserving)
;exercise
;Landau_a_th97
(axiom |∀r r0 r1.(r++r1)>>(r0++r1)⊃r>>r0|)
(label addrat_greatpreserving)
;exercise
;Landau_b_th97
(axiom |∀r r0 r1.r++r1=r0++r1⊃r=r0|)
(label great_addratpreserving)
;exercise
;Landau_th98
(axiom |∀r r0 r1 r2.r1>>r∧r2>>r0⊃(r1++r2)>>(r++r0)|)
(label great_great_addratpreserving)
;see proof below
;Landau_a_th99
(axiom |∀r r0 r1 r2.(r =< r1) ∧ (r0<<r2) ⊃ (r++r0)<<(r1++r2)|)
(label leq_less_addratpreserving)
;Landau_b_th99
(axiom |∀r r0 r1 r2.(r<<r1)∧(r0=<r2)⊃(r++r0)<<(r1++r2)|)
(label leq_less_addratpreserving)
;Landau_100
(axiom |∀r r0 r1 r2.r=<r1 ∧ r0=<r2 ⊃(r++r0)=<(r1++r2)|)
(label leq_leq_addratpreserving)
;Landau_101
(axiom |∀r r0.∃r1.r0 =< r ⊃ r++r0 = r1|)
(label minusrat)
(axiom |∀q.eqclass q++rzero=eqclass q∧
rzero++eqclass q=eqclass q|)
(label plus_rzero)(label simpinfo)
(axiom |∀r.r++rzero=r∧rzero++r=r|)
(label add_rzero)(label simpinfo)
(show *)
;multiplication of rationals
(proof multrat)
;Landau_def24
(decl multrat (type: |@r*→@r|) (infixname: |**|) (bindingpower: 949))
(defax multrat |∀r r0.(r**r0)=eqclass(tf(represent r,represent r0))|)
(label multrat)
(axiom |∀r r1.ratio(r**r1)|)
(label simpinfo)
;(trw |ef(represent(r++r1),pf(represent r,represent r1))| (open addrat)
; (use mkrepresent ))
;(trw |∀r r1.ef(represent(r**r1),tf(represent r,represent r1))|
; (open multrat) (use mkrepresent))
;∀r r1.EF(REPRESENT(r ** r1),TF(REPRESENT(r),REPRESENT(r1)))
(axiom |∀r r1.ef(represent(r ** r1),tf(represent(r),represent(r1)))|)
(label represent_ratmult)
(axiom |∀q q1.(eqclass q ** eqclass q1)=eqclass(tf(q,q1))|)
(label ratprod_reduction)
;see proof below
;Landau_th102
(axiom |∀r r1.r**r1=r1**r|)
(label commultrat)
;exercise
;Landau_th103
(axiom |∀r r1 r2.(r**r1)**r2=r**(r1**r2)|)
(label assocmultrat)
;exercise
;Landau_th104
(axiom |∀r0 r1 r2.r0**(r1++r2)=(r0**r1)++(r0**r2)|)
(label distrat)
;exercise
;Landau_a_th105 106
(axiom |∀r r1 r2.¬ rzerop r2⊃(r >> r1 ≡ (r ** r2)>>(r1 ** r2))|)
(label great_multratpreserving)
;exercise
(axiom |∀r r1 r2.¬rzerop r2⊃((r ** r2 = r1 ** r2)≡(r0=r1))|)
(label rightratcancel)
;exercise
(axiom |∀r r1 r2.¬rzerop r2⊃(r << r1 ≡ (r ** r2) << (r1 ** r2))|)
(label less_multratpreserving)
;exercise
;Landau_th107
(axiom |∀r r0 r1 r2.(r >> r1)∧(r0 >>r2)⊃ (r ** r0) >> (r1 ** r2)|)
(label Landau_th107)
;exercise
;Landau_th108
(axiom |∀r r0 r1 r2.(r >= r1)∧(r0 >> r2) ⊃ (r ** r0) >> (r1 ** r2)|)
(label Landau_a_th108)
;exercise
(axiom |∀r r0 r1 r2.(r >> r1)∧(r0 >= r2) ⊃ (r ** r0) >> (r1 ** r2)|)
(label Landau_b_th108)
;exercise
;Landau_th109
(axiom |∀r r0 r1 r2.(r >= r1)∧(r0 >= r2) ⊃ (r ** r0) >= (r1 ** r2)|)
(label Landau_th109)
;exercise
;;; (axiom |∀r r1.∃r0.r**r0=r1|)
;;; (label divrat)
;;; (axiom |∀r r1 r0 r00.r**r0=r1∧r**r00=r1⊃r0=r00|)
;;; (label divrat_uniquenesss)
;division
(decl (div) (type: |@r⊗@r→@r|)(syntype: constant))
(defax div |div=λr r1.erclass(tf(inv represent(r1),represent r))|)
(label divdef)
(axiom |∀r r1.¬rzerop r1⊃ratio(div(r,r1))|)
(label divsort)(label simpinfo)
(axiom |∀r r1.¬rzerop r1⊃(r1**div(r,r1)=r)|)
(label divisionrat)
;Landau_th110
;(derive |∀r r1.¬rzerop r1⊃(∃r2.(r1**r2)=r)| * )
;∀r r1.¬rZEROP(r1)⊃(∃r2.r1 ** r2=r)
(axiom |∀r r1.¬rzerop r1⊃(∃r2.(r1**r2)=r)|)
(label Landau_th110)
(axiom |∀r.r**rone=r∧rone**r=r|)
(label times_rone)(label simpinfo)
(show *)
;the canonical map Z-→r
(proof embedding)
(label simpinfo timesfacts)
(define inj |∀n.inj(n)=list(n,1)|)
;(trw |∀n.fr inj(n)|(open inj))
(axiom |∀n.fr inj(n)|)
(label simpinfo)
(axiom |∀n m.n>m⊃gf(inj(n),inj(m))|)
(label Landau_a_th111)
;(trw |∀n m.n=m⊃ef(inj(n),inj(m))| (open ef inj))
;∀N M.N=M⊃EF(INJ(N),INJ(M))
(axiom |∀n m.n=m⊃ef(inj(n),inj(m))|)
(label Landau_b_th111)
(axiom |∀n m.n<m⊃lf(inj(n),inj(m))|)
(label Landau_c_th111)
;Landau_def25
(define integer |∀r.integer(r)≡(∃n.ef(represent r,inj n))|)
;(trw |∀n m.ef(pf(inj(n),inj(m)),inj(n+m))| (open ef pf inj))
(axiom |∀n m.ef(pf(inj(n),inj(m)),inj(n+m))|)
(label Landau_th112)
;Landau_ax1
;(trw |integer erclass(inj 0)| (open integer inj) mkrepresent)
;INTEGER(EQCLASS(INJ(0)))
(axiom |integer(eqclass(inj(0)))|)
(label integers_peano1)
;Landau_ax2
;(trw |∀n.integer eqclass(inj(n'))| (open integer inj) mkrepresent)
;∀N.INTEGER(EQCLASS(INJ(N')))
(axiom |∀n.integer(eqclass(inj(n')))|)
(label integers_peano2)
;Landau_ax3
;(trw |∀n.¬ef(inj(n'),inj(0))| (open inj ef))
;∀N.¬EF(INJ(N'),INJ(0))
;(derive |∀n.eqclass inj(n')≠eqclass inj(0)| (* eqclass_uniqueness))
(axiom |∀n.eqclass inj(n')≠eqclass inj(0)|)
(label integers_peano3)
;Landau_ax4
;(trw |∀n m.ef(inj(n'),inj(m'))≡ef(inj n,inj m)| (open inj ef))
;∀N M.EF(INJ(N'),INJ(M'))≡EF(INJ(N),INJ(M))
;(rw * (use eqclass_uniqueness mode: always))
;∀N M.EQCLASS(INJ(N'))=EQCLASS(INJ(M'))≡EQCLASS(INJ(N))=EQCLASS(INJ(M))
(axiom |∀n m.eqclass(inj(n'))=eqclass(inj(m'))≡
eqclass(inj(n))=eqclass(inj(m))|)
(label integers_peano4)
;Landau_ax5
;(trw |∀theta.theta(inj 0)∧(∀n.theta(inj n)⊃theta(inj(n')))⊃(∀n.theta(inj n))|
; proof_by_induction)
;THETA is unknown.
;the symbol THETA declared to have type GROUND→TRUTHVAL
;∀THETA.THETA(INJ(0))∧(∀N.THETA(INJ(N))⊃THETA(INJ(N')))⊃(∀N.THETA(INJ(N)))
(axiom |∀theta.theta(inj(0))∧
(∀n.theta(inj(n))⊃theta(inj(n')))⊃(∀n.theta(inj(n)))|)
(label integer_peano5)
(axiom |∀n m.n≠0⊃(eqclass(inj(n))**eqclass list(m,n))=eqclass(inj m)|)
(label Landau_th114)
;parsing problem in the proof
(axiom |∀r r1.¬rzerop(r)⊃(∃n.((eqclass inj(n'))**r)>>r1)|)
(label Landau_th115)
;exercise
(save-proofs rat)
;*--→ noleastrat follows from noleastfr as follows:
(proof noleastrat)
;labels: NOLEASTFR
;∀q.(∃q0.LF(Q0,Q))
1. (define qv |lf(qv,represent r)| noleastfr)
;labels: EF_LF
;∀q q1 q0.EF(q,q1)∧LF(q,q0)⊃LF(q1,q0)
2. (ue ((q.qv)(q1.|represent(eqclass qv)|)(q0.|represent r|)) ef_lf
(symmf mkrepresent *))
;LF(REPRESENT(EQCLASS(qv)),REPRESENT(r))
3. (trw |(eqclass qv)<<r| * (open lessrat))
;(EQCLASS(qv)) << r
4. (derive |∃r1.r1<<r| *)
5. (derive |∀r.∃r1.r1<<r| *)
(proof density)
1. (assume |r<<r1|)
(label dense1)
2. (rw * (open lessrat))
;LF(REPRESENT(r),REPRESENT(r1))
;labels: DENSEFR
;∀q q1.(∃q0.LF(q,q1)⊃LF(q,q0)∧LF(q0,q1))
3. (define qv1 |lf(represent r,qv1)∧lf(qv1,represent r1)| (densefr *))
(label dense2)
4. (ue ((q.|represent r|)(q0.qv1)(q01.|represent(eqclass qv1)|)) lf_ef
(symmf mkrepresent *))
;LF(REPRESENT(r),REPRESENT(EQCLASS(qV1)))
;deps: (DENSE1)
5. (trw |r<<(eqclass qv1)| * (open lessrat))
;r << (EQCLASS(qV1))
(label dense3)
;deps: (DENSE1)
6. (ue ((q.qv1)(q1.|represent(eqclass qv1)|)(q0.|represent r1|)) ef_lf
(symmf mkrepresent dense2))
;LF(REPRESENT(EQCLASS(qV1)),REPRESENT(r1))
;deps: (DENSE1)
7. (trw |(eqclass qv1)<<r1| * (open lessrat))
;(EQCLASS(qV1)) << r1
(label dense4)
;deps: (DENSE1)
8. (derive |∃r0.r<<r0∧r0<<r1| (dense3 dense4))
;deps: (DENSE1)
9. (ci dense1)
;r << r1⊃(∃r0.r << r0∧r0 << r1)
10. (derive |∀r r1.r<<r1⊃(∃r0.r<<r0∧r0<<r1)| *)
;end of the proof of density
;main property of addition
(proof add_reduction)
1. (assume |ef(q00,pf(represent eqclass(q),represent eqclass(q0)))|)
;labels: SUMF_UNIQUENESS
;∀q q0 q1 q01.EF(q,q1)∧EF(q0,q01)⊃EF(PF(q,q0),PF(q1,q01))
2. (ue ((q.|represent eqclass(q)|)
(q1.|q|)
(q0.|represent eqclass(q0)|)
(q01.|q0|)) sumf_uniqueness mkrepresent)
;EF(PF(REPRESENT(EQCLASS(q)),REPRESENT(EQCLASS(q0))),PF(q,q0))
3. (derive |ef(pf(q,q0),pf(represent(eqclass(q)),represent(eqclass(q0))))|
(* symmf))
4. (ue ((q.|q1|)
(q1.|pf(represent eqclass(q),represent eqclass(q0))|)
(q2.|pf(q,q0)|)) transf -2)
;EF(q1,PF(REPRESENT(EQCLASS(q)),REPRESENT(EQCLASS(q0))))⊃EF(q1,PF(q,q0))
;labels: TRANSF
;∀q q1 q2.EF(q,q1)∧EF(q1,q2)⊃EF(q,q2)
5. (ue ((q.|q1|)
(q1.|pf(q,q0)|)
(q2.|pf(represent eqclass(q),represent eqclass(q0))|)) transf -2)
;EF(q1,PF(q,q0))⊃EF(q1,PF(REPRESENT(EQCLASS(q)),REPRESENT(EQCLASS(q0))))
6. (derive |∀q1.ef(q1,pf(represent(eqclass(q)),represent(eqclass(q0))))≡
ef(q1,pf(q,q0))| (* -2))
;labels: RATIO_EXTENSIONALITY
;∀r r1.(∀q.r(q)≡r1(q))⊃r=r1
7. (ue ((r.|eqclass(pf(represent eqclass(q),represent eqclass(q0)))|)
(r1.|eqclass(pf(q,q0))|)) ratio_extensionality * (part 1(open eqclass)))
;EQCLASS(PF(REPRESENT(EQCLASS(q)),REPRESENT(EQCLASS(q0))))=EQCLASS(PF(q,q0))
8. (trw |∀q q0.eqclass(q)++eqclass(q0)=eqclass(pf(q,q0))| * (open addrat))
;∀q q0.EQCLASS(q) ++ EQCLASS(q0)=EQCLASS(PF(q,q0))
;commaddrat
(proof commaddrat)
;labels: COMMUTFADD
;∀q q0.EF(PF(q,q0),PF(q0,q))
;labels: TRANSF
;∀q q1 q2.EF(q,q1)∧EF(q1,q2)⊃EF(q,q2)
;labels: SYMMF
;∀q q0.EF(q,q0)⊃EF(q0,q)
;labels: MKREPRESENT
;∀q.EF(REPRESENT(EQCLASS(q)),q)
;labels: TRANSF1
;∀q q1 q2 q3.EF(q,q1)∧EF(q1,q2)∧EF(q2,q3)⊃EF(q,q3)
1. (ue ((q.|represent(eqclass(pf(represent r,represent r1)))|)
(q1.|pf(represent r,represent r1)|)
(q2.|pf(represent r1,represent r)|)
(q3.|represent(eqclass(pf(represent r1,represent r)))|)) transf1
(use commutfadd ue: ((q.|represent r|)(q0.|represent r1|)) )
(use symmf ue: ((q.|represent(eqclass(pf(represent r1,represent r)))|)
(q0.|pf(represent r1,represent r)|)) )
mkrepresent )
;EF(REPRESENT(EQCLASS(PF(REPRESENT(R),REPRESENT(R1)))),
; REPRESENT(EQCLASS(PF(REPRESENT(R1),REPRESENT(R)))))
2. (derive |eqclass(pf(represent r,represent r1))=
eqclass(pf(represent r1,represent r))| (* represent_uniqueness))
3. (derive |r++r1=r1++r| * (open addrat))
;end of the proof of commaddrat
(proof assocaddrat)
;labels: SUMF_UNIQUENESS
;∀q q0 q1 q01.EF(q,q1)∧EF(q0,q01)⊃EF(PF(q,q0),PF(q1,q01))
;labels: MKREPRESENT
;∀q.EF(REPRESENT(EQCLASS(q)),q)
(ue ((q.|pf(represent r,represent r0)|)) mkrepresent)
;EF(REPRESENT(EQCLASS(PF(REPRESENT(r),REPRESENT(r0)))),
; PF(REPRESENT(Q),REPRESENT(Q0)))
1. (ue ((q.|represent(eqclass(pf(represent r,represent r0)))|)
(q1.|pf(represent r,represent r0)|)
(q0.|represent r1|)
(q01.|represent r1|)) sumf_uniqueness
* reflexf)
;EF(PF(REPRESENT(EQCLASS(PF(REPRESENT(r),REPRESENT(r0)))),REPRESENT(r1)),
; PF(PF(REPRESENT(r),REPRESENT(r0)),REPRESENT(r1)))
2. (ue ((q.|pf(represent r0,represent r1)|)) mkrepresent)
;EF(REPRESENT(EQCLASS(PF(REPRESENT(r0),REPRESENT(r1)))),
; PF(REPRESENT(r0),REPRESENT(r1)))
3. (ue ((q0.|represent(eqclass(pf(represent r0,represent r1)))|)
(q01.|pf(represent r0,represent r1)|)
(q.|represent r|)
(q1.|represent r|)) sumf_uniqueness
* reflexf)
;EF(PF(REPRESENT(r),REPRESENT(EQCLASS(PF(REPRESENT(r0),REPRESENT(r1))))),
; PF(REPRESENT(r),PF(REPRESENT(r0),REPRESENT(r1))))
;labels: SYMMF
;∀q q0.EF(q,q0)⊃EF(q0,q)
4. (ue ((q0.|pf(represent(r),pf(represent(r0),represent(r1)))|)
(q.|pf(represent(r),represent(eqclass(pf(represent(r0),represent(r1)))))|))
symmf *)
;EF(PF(REPRESENT(r),PF(REPRESENT(r0),REPRESENT(r1))),
; PF(REPRESENT(r),REPRESENT(EQCLASS(PF(REPRESENT(r0),REPRESENT(r1))))))
;labels: TRANSF1
;∀q q1 q2 q3.EF(q,q1)∧EF(q1,q2)∧EF(q2,q3)⊃EF(q,q3)
;labels: ASSOCFADD
;∀q q0 q01.PF(PF(q,q0),q01)=PF(q,PF(q0,q01))
5. (ue ((q.|pf(represent(eqclass(pf(represent(r),represent(r0)))),represent r1)|)
(q1.|pf(pf(represent(r),represent(r0)),represent(r1))|)
(q2.|pf(represent(r),pf(represent(r0),represent(r1)))|)
(q3.|pf(represent(r),represent(eqclass(pf(represent(r0),represent(r1)))))|))
transf1 -4 * reflexf
(use assocfadd ue: ((q.|represent r|)(q0.|represent r0|)(q01.|represent r1|)) ))
;EF(PF(REPRESENT(EQCLASS(PF(REPRESENT(r),REPRESENT(r0)))),REPRESENT(r1)),
; PF(REPRESENT(r),REPRESENT(EQCLASS(PF(REPRESENT(r0),REPRESENT(r1))))))
;labels: EQCLASS_UNIQUENESS
;∀Q Q0.EF(Q,Q0)⊃EQCLASS(Q)=EQCLASS(Q0)
6. (ue ((q.|pf(represent(eqclass(pf(represent(r),represent(r0)))),
represent(r1))|)
(q0.|pf(represent(r),
represent(eqclass(pf(represent(r0),represent(r1)))))|))
eqclass_uniqueness -2)
;EQCLASS(PF(REPRESENT(EQCLASS(PF(REPRESENT(r),REPRESENT(r0)))),REPRESENT(r1)))=
;EQCLASS(PF(REPRESENT(r),REPRESENT(EQCLASS(PF(REPRESENT(r0),REPRESENT(r1))))))
7. (trw |∀r r0 r1.(r++r0)++r1=r++(r0++r1)| (use addrat mode: always) *)
;∀r r0 r1.(r ++ r0) ++ r1=r ++ (r0 ++ r1)
;end of the proof of assocaddrat
;Landau_th94
;labels: LF_EF
;∀q Q0 Q01.LF(q,Q0)∧EF(Q0,Q01)⊃LF(q,Q01)
;labels: SYMMF
;∀q Q0.EF(q,Q0)⊃EF(Q0,q)
;labels: MKREPRESENT
;∀q.EF(REPRESENT(EQCLASS(q)),q)
1. (assume |¬rzerop r0|)
(label addi1)
2. (rw * (open rzerop))
;¬EF(REPRESENT(r0),qZ)
(label addi2)
;labels: SUMF_INCREASING
;∀q q0.¬EF(q0,qZ)⊃LF(q,PF(q,q0))
3. (derive |lf(represent r,pf(represent r,represent r0))| (* sumf_increasing)
(open gf))
(label addi3)
4. (ue ((q.|represent(eqclass(pf(represent r,represent r0)))|)
(q0.|pf(represent r,represent r0)|)) symmf
(use mkrepresent ue: ((r.|pf(represent r,represent r0)|)) ))
;EF(PF(REPRESENT(r),REPRESENT(r0)),
; REPRESENT(EQCLASS(PF(REPRESENT(r),REPRESENT(r0)))))
5. (ue ((q.|represent r|)
(q0.|pf(represent r,represent r0)|)
(q1.|represent(eqclass(pf(represent r,represent r0)))|))
lf_ef addi3 *)
;LF(REPRESENT(r),REPRESENT(EQCLASS(PF(REPRESENT(r),REPRESENT(r0)))))
6. (trw |∀r r1.¬rzerop(r0)⊃(r++r0)>>r| (use rzeropdef mode: exact)
(open addrat greaterrat lessrat qzerop) *)
;∀r r1.¬rZEROP(r0)⊃(r ++ r0) >> r
;deps: (ADDI1)
7. (ci addi1)
;¬rZEROP(r0)⊃(∀r.(r ++ r0) >> r)
;end of the proof of addrat_increasing
;Landau_th95
(proof great_addratpreserving)
1. (ue ((q.|represent r0|)(q0.|represent r|)(q01.|represent r1|))
lf_sumfpreserv)
;LF(REPRESENT(r0),REPRESENT(r))⊃
;LF(PF(REPRESENT(r0),REPRESENT(r1)),PF(REPRESENT(r),REPRESENT(r1)))
;labels: MKREPRESENT
;∀q.EF(REPRESENT(EQCLASS(q)),q)
2. (ue ((q.|represent(eqclass(pf(represent(r0),represent(r1))))|)
(q0.|pf(represent(r0),represent(r1))|)) symmf
(use mkrepresent mode: exact))
;EF(PF(REPRESENT(r0),REPRESENT(r1)),
; REPRESENT(EQCLASS(PF(REPRESENT(r0),REPRESENT(r1)))))
3. (ue ((q.|represent(eqclass(pf(represent(r),represent(r1))))|)
(q0.|pf(represent(r),represent(r1))|)) symmf
(use mkrepresent mode: exact))
;EF(PF(REPRESENT(r),REPRESENT(r1)),
; REPRESENT(EQCLASS(PF(REPRESENT(r),REPRESENT(r1)))))
;labels: LF_EF_EF_LF
;∀q q1 q0 q01.LF(q,q0)∧EF(q,q1)∧EF(q0,q01)⊃LF(q1,q01)
4. (ue ((q.|pf(represent(r0),represent(r1))|)
(q0.|pf(represent(r),represent(r1))|)
(q1.|represent(eqclass(pf(represent(r0),represent(r1))))|)
(q01.|represent(eqclass(pf(represent(r),represent(r1))))|))
lf_ef_ef_lf * -2)
;LF(PF(REPRESENT(r0),REPRESENT(r1)),PF(REPRESENT(r),REPRESENT(r1)))⊃
;LF(REPRESENT(EQCLASS(PF(REPRESENT(r0),REPRESENT(r1)))),
; REPRESENT(EQCLASS(PF(REPRESENT(r),REPRESENT(r1)))))
5. (derive |∀r r0 r1.r>>r0⊃(r++r1)>>(r0++r1)| (-4 *)
(open greaterrat lessrat addrat))
;end of the proof great_addratpreserving
;Landau_th98
(proof great_great_addratpreserving)
;labels: GF_GF_SUMFPRESERV
;∀q q0 q1 q01.GF(q,q0)∧GF(q1,q01)⊃GF(PF(q,q1),PF(q0,q01))
1. (ue ((q.|represent r1|)
(q0.|represent r|)
(q1.|represent r2|)
(q01.|represent r0|)) gf_gf_sumfpreserv
(open gf))
;LF(REPRESENT(r),REPRESENT(r1))∧LF(REPRESENT(r0),REPRESENT(r2))⊃
;LF(PF(REPRESENT(r),REPRESENT(r0)),PF(REPRESENT(r1),REPRESENT(r2)))
2. (ue ((q.|represent(eqclass(pf(represent(r1),represent(r2))))|)
(q0.|pf(represent(r1),represent(r2))|)) symmf
(use mkrepresent mode: exact))
;EF(PF(REPRESENT(r1),REPRESENT(r2)),
; REPRESENT(EQCLASS(PF(REPRESENT(r1),REPRESENT(r2)))))
3. (ue ((q.|represent(eqclass(pf(represent(r),represent(r0))))|)
(q0.|pf(represent(r),represent(r0))|)) symmf
(use mkrepresent mode: exact))
;EF(PF(REPRESENT(r),REPRESENT(r0)),
; REPRESENT(EQCLASS(PF(REPRESENT(r),REPRESENT(r0)))))
;labels: LF_EF_EF_LF
;∀q q1 q0 q01.LF(q,q0)∧EF(q,q1)∧EF(q0,q01)⊃LF(q1,q01)
4. (derive |lf(represent r,represent r1)∧lf(represent r0,represent r2)⊃
lf(represent(eqclass(pf(represent r,represent r0))),
represent(eqclass(pf(represent r1,represent r2))))|
(lf_ef_ef_lf -3 -2 *))
(trw |∀r r0 r1 r2.r1>>r∧r2>>r0⊃(r1++r2)>>(r++r0)| *
(open greaterrat lessrat addrat))
;∀r r0 r1 r2.r1 >> r∧r2 >> r0⊃(r1 ++ r2) >> (r ++ r0)
;end of the proof great_great_addratpreserving
;main property of multiplication
(proof timesf_reduction)
1. (assume |ef(q00,tf(represent eqclass(q),represent eqclass(q0)))|)
;labels: PRODF_UNIQUENESS
∀q q0 q1 q01.EF(q,q1)∧EF(q0,q01)⊃EF(TF(q,q0),TF(q1,q01))
2. (ue ((q.|represent eqclass(q)|)
(q1.|r|)
(q0.|represent eqclass(q0)|)
(q01.|q0|)) prodf_uniqueness mkrepresent)
;EF(TF(REPRESENT(EQCLASS(q)),REPRESENT(EQCLASS(q0))),TF(q,q0))
3. (derive |ef(tf(q,q0),tf(represent(eqclass(q)),represent(eqclass(q0))))|
(* symmf))
4. (ue ((q.|q1|)
(q1.|tf(represent eqclass(q),represent eqclass(q0))|)
(q2.|tf(q,q0)|)) transf -2)
;EF(q1,TF(REPRESENT(EQCLASS(q)),REPRESENT(EQCLASS(q0))))⊃EF(q1,TF(q,q0))
;labels: TRANSF
;∀q q1 q2.EF(q,q1)∧EF(q1,q2)⊃EF(q,q2)
5. (ue ((q.|q1|)
(q1.|tf(q,q0)|)
(q2.|tf(represent eqclass(q),represent eqclass(q0))|)) transf -2)
;EF(q1,TF(q,q0))⊃EF(q1,TF(REPRESENT(EQCLASS(q)),REPRESENT(EQCLASS(q0))))
6. (derive |∀q1.ef(q1,tf(represent(eqclass(q)),represent(eqclass(q0))))≡
ef(q1,tf(q,q0))| (* -2))
;labels: RATIO_EXTENSIONALITY
;∀r r1.(∀q.r(q)≡r1(q))⊃r=r1
7. (ue ((r.|eqclass(tf(represent eqclass(q),represent eqclass(q0)))|)
(r1.|eqclass(tf(q,q0))|)) ratio_extensionality * (part 1(open eqclass)))
;EQCLASS(TF(REPRESENT(EQCLASS(q)),REPRESENT(EQCLASS(q0))))=EQCLASS(TF(q,q0))
8. (trw |∀q q0.eqclass(q)**eqclass(q0)=eqclass(tf(q,q0))| * (open addrat))
;∀q q0.EQCLASS(q) ** EQCLASS(q0)=EQCLASS(TF(q,q0))